

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c664976 c664975)) v (c c664976 c664975))


> hypdisj
=============================
Step 3

? (c c664976 c664975)

1. (ec c664976 c664975)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c664976 c664975)

1. (~ (c c664976 c664975))
2. (ec c664976 c664975)

> hyp


LEMMA

External connection excludes overlap.
=============================
Step 1

? (all x (all y ((ec x y) => (~ (o x y)))))


> revsk
=============================
Step 2

? ((~ (ec c670105 c670104)) v (~ (o c670105 c670104)))


> hypdisj
=============================
Step 3

? (~ (o c670105 c670104))

1. (ec c670105 c670104)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 4

? (ec c670105 c670104)

1. (o c670105 c670104)
2. (ec c670105 c670104)

> hyp


LEMMA

Equality preserves connection.
=============================
Step 1

? (all x (all y (all z (((e= x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (e= c675292 c675291)) v (~ (c c675290 c675292))) v (c c675290 c675291))


> hypdisj
=============================
Step 3

? (c c675290 c675291)

1. (c c675290 c675292)
2. (e= c675292 c675291)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var26 c675291)
|
|1. (~ (c c675290 c675291))
|2. (c c675290 c675292)
|3. (e= c675292 c675291)
|
|> ((p X Y) <-- (e= X Y))
|=============================
|Step 5
|
|? (e= Var26 c675291)
|
|1. (~ (p Var26 c675291))
|2. (~ (c c675290 c675291))
|3. (c c675290 c675292)
|4. (e= c675292 c675291)
|
|> hyp
=============================
Step 6

? (c c675290 c675292)

1. (~ (c c675290 c675291))
2. (c c675290 c675292)
3. (e= c675292 c675291)

> hyp


LEMMA

Equality preserves overlap.
=============================
Step 1

? (all x (all y (all z (((e= x y) & (o z x)) => (o z y)))))


> revsk
=============================
Step 2

? (((~ (e= c680635 c680634)) v (~ (o c680633 c680635))) v (o c680633 c680634))


> hypdisj
=============================
Step 3

? (o c680633 c680634)

1. (o c680633 c680635)
2. (e= c680635 c680634)

> ((o X Z) <-- (p Y X) (p Y Z))
|=============================
|Step 4
|
|? (p Var52 c680633)
|
|1. (~ (o c680633 c680634))
|2. (o c680633 c680635)
|3. (e= c680635 c680634)
|
|> ((p Z X) <-- (~ (c (f675328 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f675328 Var52 c680633 Var55) Var52))
|
|1. (~ (p Var52 c680633))
|2. (~ (o c680633 c680634))
|3. (o c680633 c680635)
|4. (e= c680635 c680634)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f675345 Var58 Var62) Var58)
||
||1. (c (f675328 (f675345 Var58 Var62) c680633 Var55) (f675345 Var58 Var62))
||2. (~ (p (f675345 Var58 Var62) c680633))
||3. (~ (o c680633 c680634))
||4. (o c680633 c680635)
||5. (e= c680635 c680634)
||
||> ((p (f675345 X Y) X) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var58 Var62)
||
||1. (~ (p (f675345 Var58 Var62) Var58))
||2. (c (f675328 (f675345 Var58 Var62) c680633 Var55) (f675345 Var58 Var62))
||3. (~ (p (f675345 Var58 Var62) c680633))
||4. (~ (o c680633 c680634))
||5. (o c680633 c680635)
||6. (e= c680635 c680634)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f675328 (f675345 c680633 c680635) c680633 Var55) c680633))
|
|1. (c (f675328 (f675345 c680633 c680635) c680633 Var55) (f675345 c680633 c680635))
|2. (~ (p (f675345 c680633 c680635) c680633))
|3. (~ (o c680633 c680634))
|4. (o c680633 c680635)
|5. (e= c680635 c680634)
|
|> ((~ (c (f675328 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f675345 c680633 c680635) c680633))
|
|1. (c (f675328 (f675345 c680633 c680635) c680633 Var55) c680633)
|2. (c (f675328 (f675345 c680633 c680635) c680633 Var55) (f675345 c680633 c680635))
|3. (~ (p (f675345 c680633 c680635) c680633))
|4. (~ (o c680633 c680634))
|5. (o c680633 c680635)
|6. (e= c680635 c680634)
|
|> hyp
=============================
Step 10

? (p (f675345 c680633 c680635) c680634)

1. (~ (o c680633 c680634))
2. (o c680633 c680635)
3. (e= c680635 c680634)

> ((p Z X) <-- (~ (c (f675328 Z X Y) Z)))
=============================
Step 11

? (~ (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635)))

1. (~ (p (f675345 c680633 c680635) c680634))
2. (~ (o c680633 c680634))
3. (o c680633 c680635)
4. (e= c680635 c680634)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 12
|
|? (p (f675345 c680633 c680635) c680635)
|
|1. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
|2. (~ (p (f675345 c680633 c680635) c680634))
|3. (~ (o c680633 c680634))
|4. (o c680633 c680635)
|5. (e= c680635 c680634)
|
|> ((p (f675345 X Y) Y) <-- (o X Y))
|=============================
|Step 13
|
|? (o c680633 c680635)
|
|1. (~ (p (f675345 c680633 c680635) c680635))
|2. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
|3. (~ (p (f675345 c680633 c680635) c680634))
|4. (~ (o c680633 c680634))
|5. (o c680633 c680635)
|6. (e= c680635 c680634)
|
|> hyp
=============================
Step 14

? (~ (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680635))

1. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
2. (~ (p (f675345 c680633 c680635) c680634))
3. (~ (o c680633 c680634))
4. (o c680633 c680635)
5. (e= c680635 c680634)

> ((~ (c Y X)) <-- (e= X Z) (~ (c Y Z)))
|=============================
|Step 15
|
|? (e= c680635 Var78)
|
|1. (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680635)
|2. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
|3. (~ (p (f675345 c680633 c680635) c680634))
|4. (~ (o c680633 c680634))
|5. (o c680633 c680635)
|6. (e= c680635 c680634)
|
|> hyp
=============================
Step 16

? (~ (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680634))

1. (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680635)
2. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
3. (~ (p (f675345 c680633 c680635) c680634))
4. (~ (o c680633 c680634))
5. (o c680633 c680635)
6. (e= c680635 c680634)

> ((~ (c (f675328 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 17

? (~ (p (f675345 c680633 c680635) c680634))

1. (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680634)
2. (c (f675328 (f675345 c680633 c680635) c680634 Var69) c680635)
3. (c (f675328 (f675345 c680633 c680635) c680634 Var69) (f675345 c680633 c680635))
4. (~ (p (f675345 c680633 c680635) c680634))
5. (~ (o c680633 c680634))
6. (o c680633 c680635)
7. (e= c680635 c680634)

> hyp


LEMMA

From ec(x,y) and e=(y,z), derive c(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (e= y z)) => (c x z)))))


> revsk
=============================
Step 2

? (((~ (ec c686134 c686133)) v (~ (e= c686133 c686132))) v (c c686134 c686132))


> hypdisj
=============================
Step 3

? (c c686134 c686132)

1. (e= c686133 c686132)
2. (ec c686134 c686133)

> ((c Y X) <-- (e= Z X) (c Y Z))
|=============================
|Step 4
|
|? (e= Var26 c686132)
|
|1. (~ (c c686134 c686132))
|2. (e= c686133 c686132)
|3. (ec c686134 c686133)
|
|> hyp
=============================
Step 5

? (c c686134 c686133)

1. (~ (c c686134 c686132))
2. (e= c686133 c686132)
3. (ec c686134 c686133)

> ((c X Y) <-- (ec X Y))
=============================
Step 6

? (ec c686134 c686133)

1. (~ (c c686134 c686133))
2. (~ (c c686134 c686132))
3. (e= c686133 c686132)
4. (ec c686134 c686133)

> hyp


LEMMA

From ec(x,y) and e=(y,z), derive not overlap(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (e= y z)) => (~ (o x z))))))


> revsk
=============================
Step 2

? (((~ (ec c691789 c691788)) v (~ (e= c691788 c691787))) v (~ (o c691789 c691787)))


> hypdisj
=============================
Step 3

? (~ (o c691789 c691787))

1. (e= c691788 c691787)
2. (ec c691789 c691788)

> ((~ (o Y X)) <-- (e= X Z) (~ (o Y Z)))
|=============================
|Step 4
|
|? (e= c691787 Var33)
|
|1. (o c691789 c691787)
|2. (e= c691788 c691787)
|3. (ec c691789 c691788)
|
|> ((e= Y X) <-- (p Y X) (p X Y))
||=============================
||Step 5
||
||? (p c691787 Var33)
||
||1. (~ (e= c691787 Var33))
||2. (o c691789 c691787)
||3. (e= c691788 c691787)
||4. (ec c691789 c691788)
||
||> ((p Y X) <-- (e= X Y))
||=============================
||Step 6
||
||? (e= Var33 c691787)
||
||1. (~ (p c691787 Var33))
||2. (~ (e= c691787 Var33))
||3. (o c691789 c691787)
||4. (e= c691788 c691787)
||5. (ec c691789 c691788)
||
||> hyp
|=============================
|Step 7
|
|? (p c691788 c691787)
|
|1. (~ (e= c691787 c691788))
|2. (o c691789 c691787)
|3. (e= c691788 c691787)
|4. (ec c691789 c691788)
|
|> ((p X Y) <-- (e= X Y))
|=============================
|Step 8
|
|? (e= c691788 c691787)
|
|1. (~ (p c691788 c691787))
|2. (~ (e= c691787 c691788))
|3. (o c691789 c691787)
|4. (e= c691788 c691787)
|5. (ec c691789 c691788)
|
|> hyp
=============================
Step 9

? (~ (o c691789 c691788))

1. (o c691789 c691787)
2. (e= c691788 c691787)
3. (ec c691789 c691788)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 10

? (ec c691789 c691788)

1. (o c691789 c691788)
2. (o c691789 c691787)
3. (e= c691788 c691787)
4. (ec c691789 c691788)

> hyp


LEMMA

Combine c(x,z) with not o(x,z) to obtain ec(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (e= y z)) => (ec x z)))))


> revsk
=============================
Step 2

? (((~ (ec c697600 c697599)) v (~ (e= c697599 c697598))) v (ec c697600 c697598))


> hypdisj
=============================
Step 3

? (ec c697600 c697598)

1. (e= c697599 c697598)
2. (ec c697600 c697599)

> ((ec X Y) <-- (c X Y) (~ (o X Y)))
|=============================
|Step 4
|
|? (c c697600 c697598)
|
|1. (~ (ec c697600 c697598))
|2. (e= c697599 c697598)
|3. (ec c697600 c697599)
|
|> ((c X Z) <-- (ec X Y) (e= Y Z))
||=============================
||Step 5
||
||? (ec c697600 Var33)
||
||1. (~ (c c697600 c697598))
||2. (~ (ec c697600 c697598))
||3. (e= c697599 c697598)
||4. (ec c697600 c697599)
||
||> hyp
|=============================
|Step 6
|
|? (e= c697599 c697598)
|
|1. (~ (c c697600 c697598))
|2. (~ (ec c697600 c697598))
|3. (e= c697599 c697598)
|4. (ec c697600 c697599)
|
|> hyp
=============================
Step 7

? (~ (o c697600 c697598))

1. (~ (ec c697600 c697598))
2. (e= c697599 c697598)
3. (ec c697600 c697599)

> ((~ (o X Z)) <-- (ec X Y) (e= Y Z))
|=============================
|Step 8
|
|? (ec c697600 Var38)
|
|1. (o c697600 c697598)
|2. (~ (ec c697600 c697598))
|3. (e= c697599 c697598)
|4. (ec c697600 c697599)
|
|> hyp
=============================
Step 9

? (e= c697599 c697598)

1. (o c697600 c697598)
2. (~ (ec c697600 c697598))
3. (e= c697599 c697598)
4. (ec c697600 c697599)

> hyp
